Formal methods for verification of logic designs as sequential equivalence checking (SEC) technologies, capable of demonstrating the behavioral equivalence of two logic designs, have grown in capacity over the past decades. The ability to efficiently identify and leverage internal equivalence points to reduce the domain of the overall SEC problem is central to SEC scalability. However, conditionally equivalent logic designs—within which internal equivalence may not exist under sequential “observability don't care” conditions—are difficult for automated SEC tools.
Equivalence checking refers to the process of demonstrating the behavioral input-to-output equivalence of two logic designs. Numerous equivalence checking paradigms exist in practice. SEC is a generalization of a combinational equivalence checking (CEC) wherein the designs being equivalence checked may not have a 1:1 state element correlation. Due to its generality, SEC generally requires analysis of the sequential behavior of the logic designs being equivalence checked—and thus comes with substantially greater computational expense.
In J. Baumgartner, H. Mony, M. Case, J. Sawada, K. Yorav, “Scalable Conditional Equivalence Checking: An Automated Invariant-Generation Based Approach” presented at “Formal Methods in Computer-Aided Design, 2009. FMCAD 2009” an attempt is constituted to advance the scalability of SEC for conditionally equivalent designs through automated invariant generation, which enables an inductive solution to an otherwise highly noninductive problem. This technique has been demonstrated capable of yielding orders of magnitude speedup on difficult industrial conditional SEC problems.
In the paper of Baumgartner et al. a generalization of SEC is addressed: conditional sequential equivalence checking (CSEC). Unlike the above-mentioned SEC paradigm, wherein equivalence is checked at all points in time and across all execution sequences, CSEC allows designs to depart from equivalent behavior under specific time-frames. This applies, for example, to a design which pipelines its data computation across three clock periods. When a given pipeline stage is not required to produce a valid result, its clock may be disabled to reduce power consumption: a low-power technique called clock gating.
In the cited paper it is shown that a formal verification of a logic design with clock gating disabled (because it does not contribute to the essential functionality of the logic design) may produce equivalent results to a version with clock gating enabled, when the formal verification is performed by equivalence checking with itself.
In other approaches, random input sequences are used for guiding the simulation of highly optimized pipelines. However, random input sequences fail to effectively provide coverage of unique window and corner conditions. Subsequent quasi-random, biased approaches utilize optimization criteria that increase coverage only linearly and are not exhaustive.
Formal approaches require extensive assertion coding for state-space exploration and are limited in scope to smaller circuits. Thus, it is desirable to verify all sequences for complete coverage, while also avoiding the cost and size limitations of other formal approaches.